/* Benchmarks for the PionterC verifier. */

// list visit

struct list 
{
  int data;
  struct list* next;
};

/*@ 
  @*/
struct list* creatList(int n)
{
  struct list* l;
  struct list* p;
  int i;
  
    p = null;
    l = null;
    //p->next = null;
  
  if (n>0) {
    i = 0;
    while(i<=n-1) /*@({p, l}N) 
                    || (({p, l}) && list(l->next)) 
                    */ 
    {
      p = alloc(struct list);
      // p = alloc(struct list);
      p->next = l;
      l = p;
      i = i+1;
    }
    
  } 
 return l;
}
/*@ */
  
